@string{CUCL="Computer Laboratory, University of Cambridge"}
@string{CUP="Cambridge University Press"}

@TechReport{camilleri92,
  author	= {J. Camilleri and T. F. Melham},
  title		= {Reasoning with Inductively Defined Relations in the
		 {HOL} Theorem Prover},
  institution	= CUCL,
  year		= 1992,
  number	= 265,
  month		= Aug}

@InProceedings{paulin-tlca,
  author	= {Christine Paulin-Mohring},
  title		= {Inductive Definitions in the System {Coq}: Rules and
		 Properties},
  crossref	= {tlca93},
  pages		= {328-345}}

@Proceedings{tlca93,
  title		= {Typed Lambda Calculi and Applications},
  booktitle	= {Typed Lambda Calculi and Applications},
  editor	= {M. Bezem and J.F. Groote},
  year		= 1993,
  publisher	= {Springer},
  series	= {LNCS 664}}

@InCollection{szasz93,
  author	= {Nora Szasz},
  title		= {A Machine Checked Proof that {Ackermann's} Function is not
		  Primitive Recursive},
  crossref	= {huet-plotkin93},
  pages		= {317-338}}

@book{huet-plotkin93,
  editor	= {{G{\'e}rard} Huet and Gordon Plotkin},
  title		= {Logical Environments},
  booktitle	= {Logical Environments},
  publisher	= CUP,
  year		= 1993}

@book{mendelson,
  Author = {E. Mendelson},
  Edition = {Fourth},
  Publisher = {Chapman \& Hall},
  Title = {Introduction to Mathematical Logic},
  Year = {1997}}

